(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const _14-0 (_ BitVec 14))
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const _12-6 (_ BitVec 12))
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const v22 Bool)
(declare-const _14-3 (_ BitVec 14))
(declare-const v23 Bool)
(declare-const _19-0 (_ BitVec 19))
(declare-const v24 Bool)
(declare-const v25 Bool)
(declare-const v26 Bool)
(declare-const v27 Bool)
(declare-const v28 Bool)
(declare-const _8-0 (_ BitVec 8))
(declare-const v29 Bool)
(declare-const v30 Bool)
(declare-const v31 Bool)
(declare-const v32 Bool)
(declare-const v33 Bool)
(declare-const v34 Bool)
(declare-const v35 Bool)
(declare-const v36 Bool)
(declare-const v37 Bool)
(declare-const v38 Bool)
(declare-const v39 Bool)
(declare-const _14-5 (_ BitVec 14))
(declare-const v40 Bool)
(declare-const _20-0 (_ BitVec 20))
(declare-const _16-0 (_ BitVec 16))
(declare-const v41 Bool)
(declare-const _28-0 (_ BitVec 28))
(declare-const v42 Bool)
(declare-const v43 Bool)
(declare-const v44 Bool)
(declare-const _5-0 (_ BitVec 5))
(declare-const v45 Bool)
(declare-const v46 Bool)
(declare-const v47 Bool)
(assert (forall ((q11 Bool)) (not (or (distinct (_ bv11 4) (bvxor ((_ extract 3 0) (_ bv53 6)) ((_ extract 3 0) (_ bv53 6)) (_ bv11 4) (_ bv11 4)) ((_ extract 3 0) (_ bv53 6)) (bvxor ((_ extract 3 0) (_ bv53 6)) ((_ extract 3 0) (_ bv53 6)) (_ bv11 4) (_ bv11 4)) (bvxor ((_ extract 3 0) (_ bv53 6)) ((_ extract 3 0) (_ bv53 6)) (_ bv11 4) (_ bv11 4))) (not v16) q11 v0 (=> (xor (= (bvsrem #b1100000111 #b1100000111) (bvxor (bvsrem #b1100000111 #b1100000111) (bvashr #b1100000111 #b1100000111) (bvashr #b1100000111 #b1100000111) (bvsrem #b1100000111 #b1100000111)) (bvashr #b1100000111 #b1100000111)) (or (=> v2 v3) v7 v8 (=> v2 (=> v3 v3)) (or v4 v0 v3 v4) (bvsle #b1100000111 #b1001011001)) (distinct v7 v13 (bvsle #b1100000111 #b1001011001) v0 (or v4 v0 v3 v4) (distinct _14-0 _14-0 _14-0 _14-0) v0 (=> v2 (=> v3 v3)) v7 v10 v5) (=> v2 v3) v19 v25 v25 v7 (=> v2 v3) (distinct ((_ repeat 3) (bvashr #x39c #x39c)) ((_ repeat 3) (bvashr #x39c #x39c)) ((_ repeat 3) (bvashr #x39c #x39c)) ((_ repeat 3) (bvashr #x39c #x39c))) v23) v9) q11 q11 q11))))
(check-sat)
